Nuprl Lemma : l_disjoint_member
4,23
postcript
pdf
T
:Type,
l1
,
l2
:
T
List,
x
:
T
. l_disjoint(
T
;
l1
;
l2
)
(
x
l1
)
(
x
l2
)
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
(
x
l
)
,
Prop
,
P
&
Q
,
A
,
P
Q
,
False
,
l_disjoint(
T
;
l1
;
l2
)
,
True
Lemmas
not
wf
,
l
member
wf
origin
T:Type, l1, l2:T List, x:T. l_disjoint(T;l1;l2) 
(x 
l1) 
(x l2) T:Type, l1, l2:T List, x:T. l_disjoint(T;l1;l2) (x l1) (x l2) Tx:A. B(x) l)A Q